$\forall$${\it the\_es}$:ES, ${\it e'}$:E, $n$:$\mathbb{N}$.
\\[0ex]($n$ $<$ $\parallel$before(${\it e'}$)$\parallel$) $\Rightarrow$ (firstn($n$;before(${\it e'}$)) = before(before(${\it e'}$)[$n$]) $\in$ (E List))